Nuprl Lemma : dsys-sub-join-left
0,22
postcript
pdf
A
,
B
:Dsys.
A
A
B
latex
Definitions
t
T
,
Dsys
,
MsgA
,
x
:
A
.
B
(
x
)
,
Id
,
M1
M2
,
M(
i
)
,
D1
D2
,
A
B
Lemmas
dsys
wf
,
Id
wf
,
ma-sub-join-left
origin
A, B:Dsys. A 
A 
B A, B:Dsys. A A B 
Tx:A. B(x) M2 D2 B